fix(symbolic): include the cheatcode address in EXTCODE* candidates by figtracer · Pull Request #18330 · foundry-rs/foundry

figtracer · 2026-11-09T22:49:24Z

Why

Before: Symbolic EXTCODE operations missed the cheatcode addresses. Symbolic calls also sent unknown selectors at the compatibility address through Forge's cheatcode decoder, which could falsely prove an assertion.

After: EXTCODE covers those addresses, and an unknown compatibility-address call can produce a replayed counterexample.

Change

Include the special addresses in EXTCODE candidates. Keep Forge decoder errors at the real cheatcode address, and treat unknown compatibility selectors as ordinary EVM calls while preserving the recognized symbolic-VM operations.

Downstream

forge test --symbolic results change for these address aliases; no API, configuration, or persisted-data format changes. AI assistance was used.

Forge gives the cheatcode address the one-byte code 0x00. The candidate set for a symbolic address left it out, so EXTCODESIZE, EXTCODEHASH, and EXTCODECOPY never considered it and a property that fails at address(vm) passed. `known_addresses` now includes the cheatcode addresses, as `balance_word` already did, and symbolic call targets keep skipping them.

mattsse

Please reconcile the existing high-level CALL regression with the newly included cheatcode candidates.

mattsse · 2026-11-09T23:01:40Z

-            .filter(|address| {
-                *address != CHEATCODE_ADDRESS && *address != SYMBOLIC_VM_COMPAT_ADDRESS
-            })
+            .chain([CHEATCODE_ADDRESS, SYMBOLIC_VM_COMPAT_ADDRESS])


Update the high-level CALL regression for the new candidates

Including these addresses makes Solidity's EXTCODESIZE guard admit cheatcode targets, but symbolic_call_targets still excludes them. With the default symbolic_call_targets = false, checkUnconstrainedHighLevelCall(address) therefore returns incomplete symbolic execution (Stuck): unsupported symbolic execution feature: symbolic CALL target instead of the replayed assertion failure still expected by symbolic_account_queries_see_setup_accounts. This snapshot fails on all three attempts in test / test all. Please reconcile the CALL handling or update that regression's expectation in this PR so the required suite passes.

With the cheatcode address as an EXTCODESIZE candidate, a high-level call to an unconstrained target reaches CALL with the cheatcode address as a feasible target, which the call-target split reported as unsupported. Model it like Forge: a call to the cheatcode addresses with an unknown selector reverts, and a cheatcode selector stays unsupported. The call candidates themselves are unchanged.

mattsse

The prior CI regression is fixed. Two correctness issues remain in the new symbolic cheatcode-call branch.

mattsse · 2026-11-10T00:35:30Z

+            {
+                return Err(SymbolicError::Unsupported("symbolic cheatcode CALL target"));
+            }
+            let return_data = SymReturnData::empty(&mut self.cx);


Preserve the unknown-selector revert payload

Concrete Forge returns ABI-encoded CheatcodeError(...) for an unknown selector (apply_cheatcode constructs the error and the inspector ABI-encodes it), rather than empty bytes. For example, constrain target to address(vm) or a deployed Pinger, perform target.call(abi.encodeWithSignature("ping()")), and assert that the returned bytes have length zero. The normal Pinger.ping() returns no bytes, and this new branch also supplies no bytes, so the symbolic model can prove that assertion even though the concrete VM case fails it. Please preserve the concrete error payload, or report incomplete for this case until it is modeled.

mattsse · 2026-11-10T00:35:30Z

+                return Err(SymbolicError::Unsupported("symbolic cheatcode CALL target"));
+            }
+            let return_data = SymReturnData::empty(&mut self.cx);
+            match self.finish_codeless_call(


Keep revert expectations pending across cheatcode calls

finish_codeless_call consumes a pending ordinary vm.expectRevert, but concrete Forge explicitly skips cheatcode calls in ExpectedRevert::needs_processing. Consider vm.expectRevert(); target.call(abi.encodeWithSignature("ping()")); pinger.ping();, with target constrained to the VM address or a contract whose fallback reverts. This branch treats the VM's unknown-selector revert as satisfying the expectation, so the subsequent successful ping() passes. Concrete Forge leaves the expectation pending and fails that subsequent call with next call did not revert as expected. Please retain the cheatcode-specific handling here; the same helper also incorrectly consumes pending assumeNoRevert state for this branch.

A symbolic call that may alias the cheatcode address now reverts with the `CheatcodeError(string)` payload Forge's `decode_cheatcode_call` produces for the selector instead of empty bytes, so return data checks agree with the concrete run. The branch completes through `revert_cheatcode_call`, which, like Forge, leaves a pending `vm.expectRevert` or `vm.assumeNoRevert` for the next non-cheatcode call. `decode_cheatcode_call` and `revert_cheatcode_call` are shared with #18335.

mattsse

The previous findings are fixed. One compatibility-address CALL issue remains.

mattsse · 2026-11-10T01:40:05Z

+        // The cheatcode addresses have code, so an unconstrained target may alias them. They are
+        // not call candidates: Forge fails a call to them that its cheatcode decoder rejects.
+        let cheatcode_constraints =
+            [CHEATCODE_ADDRESS, SYMBOLIC_VM_COMPAT_ADDRESS].map(|address| {


Separate compatibility aliases from Forge cheatcode decoding

SYMBOLIC_VM_COMPAT_ADDRESS is not intercepted by the concrete Forge cheatcode inspector: in an ordinary unforked test it has no code, so a low-level ping() call succeeds. Grouping it with CHEATCODE_ADDRESS sends it through decode_cheatcode_call and forces a revert instead. For example, constrain target to the compatibility address or a deployed contract with a reverting fallback, call target.call(abi.encodeWithSignature("ping()")), and assert !success: both branches now revert symbolically, while the compatibility-address input concretely succeeds and violates the assertion. The existing engine with --symbolic-call-targets finds and replays exactly that counterexample. Please split the compatibility-address handling and report incomplete if its semantics cannot be modeled, rather than fabricating a Forge decoder revert.

The symbolic VM compatibility address is not a Forge cheatcode target for unknown selectors. Route only recognized symbolic-VM selectors through its handler, and include the compatibility address among symbolic call candidates so a normal successful call cannot be falsely proven to revert.

mattsse

The earlier findings are fixed. The new ordinary compatibility-call path still ignores installed code.

mattsse · 2026-11-10T04:38:19Z

+                let selector: [u8; 4] = selector
+                    .try_into()
+                    .map_err(|_| SymbolicError::Unsupported("symbolic compatibility selector"))?;
+                SymbolicVmCheatcode::from_selector(selector).is_some()


Execute the installed code for ordinary compatibility calls

Unknown selectors now fall through to normal CALL execution, but that path loads its child code through SymbolicWorld::extcode, which still unconditionally returns a synthetic STOP byte for the compatibility address before consulting code_cache or the backend. For example, vm.etch(COMPAT, hex"60006000fd"); (bool ok,) = COMPAT.call(hex"5c36b186"); assert(ok); now executes STOP symbolically and can pass, although concrete Forge executes the installed REVERT and fails the assertion. Previously this unknown compatibility selector reported incomplete. Please make this ordinary-call path honor the account's installed code, or fail closed when that code cannot be modeled.

stevencartavia · 2026-11-10T05:27:38Z

        }

        let call_input = in_size.read_from_memory(&mut self.cx, &state.memory, in_offset.clone());
+        let mut cheatcode_branch = state.clone();


The cheatcode branch doesn't check the call kind. Forge only intercepts when destination == CHEATCODE_ADDRESS, so DELEGATECALL and CALLCODE to address(vm) run its 0x00 code and succeed. Modelling them as a decoder revert makes assert(!ok) falsely pass. With --symbolic-call-targets, base reported a correct counterexample here. Build this branch only for Call/StaticCall.

figtracer requested review from 0xrusowsky, DaniPopes, grandizzy, mablr, mattsse and stevencartavia as code owners November 9, 2026 22:49

mattsse requested changes Nov 9, 2026

View reviewed changes

figtracer requested a review from mattsse November 9, 2026 23:44

mattsse requested changes Nov 10, 2026

View reviewed changes

figtracer requested a review from mattsse November 10, 2026 01:34

mattsse requested changes Nov 10, 2026

View reviewed changes

figtracer requested a review from mattsse November 10, 2026 04:28

mattsse requested changes Nov 10, 2026

View reviewed changes

stevencartavia reviewed Nov 10, 2026

View reviewed changes

Navigation Menu

Repository navigation

fix(symbolic): include the cheatcode address in EXTCODE* candidates - #18330

fix(symbolic): include the cheatcode address in EXTCODE* candidates#18330
figtracer wants to merge 4 commits into
mablr/evm2-migrationfrom
fig/symbolic-extcode-cheatcode-address

figtracer commented Nov 9, 2026 •

edited

Loading

Uh oh!

mattsse left a comment

Uh oh!

mattsse Nov 9, 2026

Uh oh!

mattsse left a comment

Uh oh!

mattsse Nov 10, 2026

Uh oh!

mattsse Nov 10, 2026

Uh oh!

mattsse left a comment

Uh oh!

mattsse Nov 10, 2026

Uh oh!

mattsse left a comment

Uh oh!

mattsse Nov 10, 2026

Uh oh!

stevencartavia Nov 10, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

figtracer commented Nov 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Why

Change

Downstream

Uh oh!

mattsse left a comment

Choose a reason for hiding this comment

Uh oh!

mattsse Nov 9, 2026

Choose a reason for hiding this comment

Uh oh!

mattsse left a comment

Choose a reason for hiding this comment

Uh oh!

mattsse Nov 10, 2026

Choose a reason for hiding this comment

Uh oh!

mattsse Nov 10, 2026

Choose a reason for hiding this comment

Uh oh!

mattsse left a comment

Choose a reason for hiding this comment

Uh oh!

mattsse Nov 10, 2026

Choose a reason for hiding this comment

Uh oh!

mattsse left a comment

Choose a reason for hiding this comment

Uh oh!

mattsse Nov 10, 2026

Choose a reason for hiding this comment

Uh oh!

stevencartavia Nov 10, 2026

Choose a reason for hiding this comment

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

figtracer commented Nov 9, 2026 •

edited

Loading